Publish documentation #7149

markrtuttle · 2022-09-22T02:26:48Z

This pull request proposes a method of publishing documentation in the diffblue/cbmc repository to the diffblue.github.io/cbmc web site. See this comment for a discussion of the goals. See markrtuttle.github.io/cbmc-documentation for a demonstration.

After merging this pull request, the diffblue/cbmc repository must be configured to publish pages from the branch gh-pages to diffblue.github.io/cbmc. See github instructions to configure from within the account settings (basically two clicks).

There are many known issues. A lot of these comments have to do with using pandoc to remove doxygen issues from markdown files before running doxygen. It is nearly impossible to write markdown files that format cleanly with doxygen and two versions of pandoc and still read well on github as rendered markdown (and still work well with the javascript rendering www.cprover.org/cprover-manual). The biggest issue is that doxygen is written to render markdown snippets from code comments, but does not handle well a collection of basic markdown files that interlink among themselves using classical markdown syntax. Most important, doxygen wants explicitly-declared, globally-unique labels in markdown (that is not supported by classical markdown) for links, and does not follow markdown syntax for linking to sections within a markdown file. We need to make a decision about whether we are writing markdown or doxygen markdown. I recommend (sigh) doxygen markdown and using \page unique-label Heading in place of # Heading. For section labels, without requiring unique section names, the only option appears to be \section unique-label Section in place of ## Section, but that is a massive revision (or just give up on linking directly to section headers).

The modern brew doxygen is 1.9.5 and the ubuntu-latest doxygen on github is 1.8.17. The older version 1.8.17 appears to differ slightly between brew and ubuntu (eg, volume of progress information printed during execution). The newer version 1.9.5 issues warnings that the older version 1.8.17 does not. Differences include some unused variables in doxyfile that are now obsolete, and 500+ new warnings of the form

cbmc/src/util/std_types.h:736: 
   warning: unable to resolve reference to 'code_typet.\ifile' for \ref command

This pull request restores two files that may have been deleted from develop:
- doc/architectural/restrict-function-pointer.md
- doc/architectural/nondet-volatile.md

goto-cc has broken links (what should they link to?):

-   \ref man_goto-cc-linux "Linux Kernel"
-   \ref man_goto-cc-apache "Apache HTTPD"

test_suite.md a broken link (what should it link to?):
```
[pid\_test\_suites.xml](pid_test_suites.xml)
```
pandoc cannot handle lists or rules that are not preceded by a blank line. In particular, it will try to interpret text immediately following the horizontal rule --- as yaml.
pandoc --read markdown sometimes treats doxygen commands like \ingroup as latex commands. Using pandoc --read markdown_phpextra avoids this problem.
pandoc --read markdown_phpextra sometimes deletes or modifies fenced code blocks with syntax highlighting like ```c. Using pandoc --read markdown avoids this problem.
doxygen cannot handle links [hyper link](url) that break over two lines. Using pandoc --wrap none solves this problem, but now what to use for --read and --write formats (see above).
cprover-manual has mutliple sections with same title resulting in nonunique labels for doxygen. Doxygen cannot link to internal sections with [section](#section). Doxygen requires globally unique section labels. This is not supported in straight markdown. The pandoc --write markdown_phpextra will generate the needed section labels, but doxygen complains because they are not unique. For example, in the contracts pages, there are multiple sections named "Overview".
cprover-manual does not have top-level sections, and doxygen complains it has subsections outside of sections, etc.

* Replace top-level section headings with \page command * Ensure a space between \ingroup and \page for pandoc parsing * Remove link to cprover-manual index from memory-analyzer, restrict-function pointer, etc, and make these pages subpages of the top-level architectural page

* Format index.md as nested lists instead of a list of section headings * Correct broken links * Add blank link before all lists for pandoc parsing * Some end-of-line whitespace removed

* Add README files of doc/API and src/goto-harness * Add surround markdown horizontal rule --- with blank lines for pandoc parsing (pandoc will try to interpret text following --- as yaml).

* Append "last modified" dates to the end of all markdown files. * Use a pandoc filter to rewrite links in cprover-manual (links originally intended to work with the cprover.org/cprover-manual javascripts). * Add a script to repair fenced code blocks written by pandoc

* doc/ADR * doc/API * doc/assets * doc/cprover-manual

Add top-level user guide, reference guide, developer guide pages for the new published documentation. The top-level doxyfile is the original src/doxyfile with minor modification (eg, project title is now "CBMC").

codecov · 2022-09-22T04:11:14Z

Codecov Report

Base: 77.87% // Head: 77.88% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (ee0a06d) compared to base (3034749).
Patch has no changes to coverable lines.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7149   +/-   ##
========================================
  Coverage    77.87%   77.88%           
========================================
  Files         1576     1576           
  Lines       181824   181867   +43     
========================================
+ Hits        141598   141645   +47     
+ Misses       40226    40222    -4

Impacted Files	Coverage Δ
src/util/format_expr.cpp	`86.89% <0.00%> (-0.47%)`	⬇️
src/util/graph.h	`96.83% <0.00%> (-0.32%)`	⬇️
src/ansi-c/expr2c.cpp	`67.13% <0.00%> (-0.05%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`74.19% <0.00%> (-0.01%)`	⬇️
src/util/simplify_expr_class.h	`90.47% <0.00%> (ø)`
src/goto-symex/goto_symex_state.h	`100.00% <0.00%> (ø)`
src/goto-programs/validate_goto_model.h	`100.00% <0.00%> (ø)`
src/goto-programs/validate_goto_model.cpp	`100.00% <0.00%> (ø)`
unit/goto-programs/goto_program_validate.cpp	`100.00% <0.00%> (ø)`
src/goto-programs/restrict_function_pointers.h	`100.00% <0.00%> (ø)`
... and 9 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

doc/architectural/front-page.md

doc/architectural/nondet-volatile.md

doc/architectural/restrict-function-pointer.md

tautschnig · 2022-09-22T13:17:23Z

doc/cprover-manual/index.md

+1. [Introduction](introduction/)

-## 2. [Installation](installation/)
+2. [Installation](installation/)


@kroening Will this render ok on cprover.org?

FWIW, I did mention this to @kroening (replacing the sequence of headers with a list) and he did not object.

tautschnig · 2022-09-22T13:19:00Z

doc/doxygen-root/doxygen-markdown/markdown.sh

+# Note: Need to read markdown as markdown_phpextra and not default
+# markdown to preserve doxygen pragmas like \ingroup.
+
+# Bug: This is currently interacting badly with \dot in cprover markdown


To what extent should we be concerned about this? Is there any plan to do something about this?

This preprocessing is required on the cprover-manual pages as long as they are served up by javascript on prover.org. I did a quick scan of the architectural pages, and I saw no obvious problems caused by omitting this preprocessing on the current set of pages. But I think doxygen's brittle treatment of markdown files is a potential issue, and I think we would be better off just deciding to write doxygen-friendly markdown and just living with subpar rendering by other tools (like on github).

doc/doxygen-root/doxyfile

The content of nondet-volatile.md and restrict-function-pointer.md in doc/architectural has already been moved to the goto-instrument man page. Remove this also from architectural main page front-page.md

This doxygen file is based on src/doxyfile, and src/doxyfile can be removed once the run_doxygen continuous integration check is disabled.

jimgrundy · 2022-09-23T14:06:18Z

I'd like to see this adopted so that documentation can be maintained more easily and directly from GitHub, and browsable within GitHub and local repos. Further, I'd like to see is declare "Doxygen" and "MarkDown as spoken by Doxygen" become our expected documentation method, which would allow us to strip away a little of the scripting complexity Mark added to support the Markdown as it is today. But, that can wait. Please let's get this in.

NlightNFotis · 2022-09-23T14:08:30Z

@jimgrundy Hi Jim, this is on my plate for today - will get this reviewed, but then I'm not sure who else this needs reviews from. I'll see if it needs a couple more from our end if I can chase them further (but please be aware that we've been hit by unexpected illness in our team, so we're missing some of our usual bandwidth).

NlightNFotis

Some minor comments that don't diminish the ability of this to move forward.

Thank you for your efforts to bring the documentation up to date.

NlightNFotis · 2022-09-23T15:03:02Z

doc/API/README.md

@@ -0,0 +1,3 @@
+# CProver APIs


This should be changed to something like:

\page apis CPROVER APIs

This particular proposal won't work because this is the main markdown file for doc/API. The folders doc/API, doc/ADR, and doc/assets are built separately because they don't seem to be linked into the main CPROVER documentation.

I've taken the liberty of converting doc/API and doc/ADR to the doxygen page/subpage syntax.

I was going to do the same for doc/assets, but there is an xml-spec.md that is not linked to by the top-level README, and I wasn't sure which of the various specs are considered authoritative.

@NlightNFotis

NlightNFotis · 2022-09-23T15:29:45Z

doc/doxygen-root/README.md

+* On MacOS,
+  we recommend installing with [brew](https://brew.sh/):
+  ```
+  brew install doxygen graphviz


Does this need pandoc as well?

I tried without and got some errors?

I've added pandoc to the instructions. I omitted it because it is already installed on the GitHub ubuntu runner. But good catch.

NlightNFotis · 2022-09-23T15:31:15Z

doc/doxygen-root/README.md

+To build the documentation, run
+
+```
+doxygen


There's also a Makefile.

I tried running the default action of the Makefile first, but got a very broken version of the documentation (probably because I was missing stuff from the dependencies?) - which one is the defacto way a developer builds documentation locally? Just running Doxygen, or the Makefile?

Good catch. There is now a makefile to automate the five or six invocations of doxygen. The current build command is "make".

NlightNFotis · 2022-09-23T15:31:45Z

doc/doxygen-root/README.md

+
+## Contribute documentation
+
+Coming soon...


There appears to be some documentation on this at contributing.md.

Added a link. Thanks.

NlightNFotis · 2022-09-23T15:32:12Z

doc/doxygen-root/README.md

@@ -0,0 +1,60 @@
+# CBMC documentation


Should this readme file be lifted to the top-level of the documentation folder, or does it conflict with the compilation of the documentation?

I could go either way. My intention is that this documents the process of building the documentation, and so doesn't belong in the documentation itself. I'm leaving it out for now.

feliperodri · 2022-09-23T19:13:05Z

doc/doxygen-root/developer_guide.md

+* \ref cprover_documentation
+  * [CProver Architecture Decision Records](adr/index.html)
+  * [CProver APIs](api/index.html)
+  * [CProver assets](assets/index.html)


nitpick: s/assets/Assets/g

markrtuttle requested review from a team, tautschnig, feliperodri, remi-delmas-3000, martin-cs, chris-ryder, peterschrammel, kroening and romainbrenguier as code owners September 22, 2022 02:26

Mark R. Tuttle added 8 commits September 21, 2022 22:36

Make cprover-manual format nicely with doxygen

dd1b0e0

* Format index.md as nested lists instead of a list of section headings * Correct broken links * Add blank link before all lists for pandoc parsing * Some end-of-line whitespace removed

Make three README files format with doxygen/pandoc

d41591b

* Add README files of doc/API and src/goto-harness * Add surround markdown horizontal rule --- with blank lines for pandoc parsing (pandoc will try to interpret text following --- as yaml).

Make satabs user manual a first-class page

b11af9b

Add doxyfiles for miscellaneous sets of markdown files

142bfac

* doc/ADR * doc/API * doc/assets * doc/cprover-manual

Add top-level documtation pages

ecfd0de

Add top-level user guide, reference guide, developer guide pages for the new published documentation. The top-level doxyfile is the original src/doxyfile with minor modification (eg, project title is now "CBMC").

Add cbmc documentation publication workflow

ec26ef5

markrtuttle force-pushed the publish-documentation branch from 8261342 to ec26ef5 Compare September 22, 2022 02:39

feliperodri added documentation aws Bugs or features of importance to AWS CBMC users labels Sep 22, 2022

tautschnig approved these changes Sep 22, 2022

View reviewed changes

tautschnig assigned kroening, NlightNFotis and peterschrammel Sep 22, 2022

tautschnig mentioned this pull request Sep 22, 2022

Rendered doxygen is out of date and needs further work #7112

Closed

3 tasks

Mark R. Tuttle added 3 commits September 22, 2022 13:37

Remove a blank line from the top of a markdown file

b498483

Remove "nondet volatile" and "function pointer" pages from user guide

5969edd

The content of nondet-volatile.md and restrict-function-pointer.md in doc/architectural has already been moved to the goto-instrument man page. Remove this also from architectural main page front-page.md

Update doc/doxygen-root/doxyfile to version 1.8.17

947d3f3

This doxygen file is based on src/doxyfile, and src/doxyfile can be removed once the run_doxygen continuous integration check is disabled.

markrtuttle force-pushed the publish-documentation branch from 1eb7041 to 947d3f3 Compare September 22, 2022 20:36

tautschnig unassigned kroening Sep 22, 2022

jimgrundy added the aws-high label Sep 23, 2022

NlightNFotis approved these changes Sep 23, 2022

View reviewed changes

feliperodri approved these changes Sep 23, 2022

View reviewed changes

peterschrammel approved these changes Sep 24, 2022

View reviewed changes

Mark R. Tuttle added 3 commits September 25, 2022 17:48

Correct and elaborate the documentation-build documentation

7e9f21e

Fix typo in developer guide

f44d11e

Convert doc/ADR and doc/API to doxygen page/subpage syntax

ee0a06d

markrtuttle force-pushed the publish-documentation branch from 0781a2a to ee0a06d Compare September 25, 2022 22:48

NlightNFotis merged commit 5834261 into diffblue:develop Sep 26, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Publish documentation #7149

Publish documentation #7149

markrtuttle commented Sep 22, 2022 •

edited

Loading

codecov bot commented Sep 22, 2022 •

edited

Loading

tautschnig Sep 22, 2022

markrtuttle Sep 22, 2022

tautschnig Sep 22, 2022

markrtuttle Sep 22, 2022

jimgrundy commented Sep 23, 2022

NlightNFotis commented Sep 23, 2022 •

edited

Loading

NlightNFotis left a comment

NlightNFotis Sep 23, 2022

markrtuttle Sep 25, 2022 •

edited

Loading

NlightNFotis Sep 23, 2022

markrtuttle Sep 25, 2022

NlightNFotis Sep 23, 2022

markrtuttle Sep 25, 2022

NlightNFotis Sep 23, 2022

markrtuttle Sep 25, 2022

NlightNFotis Sep 23, 2022

markrtuttle Sep 25, 2022

feliperodri Sep 23, 2022 •

edited

Loading

markrtuttle Sep 25, 2022

Publish documentation #7149

Publish documentation #7149

Conversation

markrtuttle commented Sep 22, 2022 • edited Loading

codecov bot commented Sep 22, 2022 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jimgrundy commented Sep 23, 2022

NlightNFotis commented Sep 23, 2022 • edited Loading

NlightNFotis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

markrtuttle Sep 25, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

feliperodri Sep 23, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

markrtuttle commented Sep 22, 2022 •

edited

Loading

codecov bot commented Sep 22, 2022 •

edited

Loading

NlightNFotis commented Sep 23, 2022 •

edited

Loading

markrtuttle Sep 25, 2022 •

edited

Loading

feliperodri Sep 23, 2022 •

edited

Loading